Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar14/variousSLASH08.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

f1₂(a, x) -> g1₂(x, x)
f1₂(x, a) -> g2₂(x, x)
f2₂(a, x) -> g1₂(x, x)
f2₂(x, a) -> g2₂(x, x)
g1₂(a, x) -> h1₁(x)
g1₂(x, a) -> h2₁(x)
g2₂(a, x) -> h1₁(x)
g2₂(x, a) -> h2₁(x)
h1₁(a) -> i
h2₁(a) -> i
e1₆(h1₁(w), h2₁(w), x, y, z, w) -> e2₆(x, x, y, z, z, w)
e1₆(x1, x1, x, y, z, a) -> e5₄(x1, x, y, z)
e2₆(f1₂(w, w), x, y, z, f2₂(w, w), w) -> e3₁₂(x, y, x, y, y, z, y, z, x, y, z, w)
e2₆(x, x, y, z, z, a) -> e6₃(x, y, z)
e2₆(i, x, y, z, i, a) -> e6₃(x, y, z)
e3₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> e4₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3₁₂(x, y, x, y, y, z, y, z, x, y, z, a) -> e6₃(x, y, z)
e4₁₂(g1₂(w, w), x1, g2₂(w, w), x1, g1₂(w, w), x1, g2₂(w, w), x1, x, y, z, w) -> e1₆(x1, x1, x, y, z, w)
e4₁₂(i, x1, i, x1, i, x1, i, x1, x, y, z, a) -> e5₄(x1, x, y, z)
e4₁₂(x, x, x, x, x, x, x, x, x, x, x, a) -> e6₃(x, x, x)
e5₄(i, x, y, z) -> e6₃(x, y, z)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f1₂(a, x) -> g1₂(x, x)
f1₂(x, a) -> g2₂(x, x)
f2₂(a, x) -> g1₂(x, x)
f2₂(x, a) -> g2₂(x, x)
g1₂(a, x) -> h1₁(x)
g1₂(x, a) -> h2₁(x)
g2₂(a, x) -> h1₁(x)
g2₂(x, a) -> h2₁(x)
h1₁(a) -> i
h2₁(a) -> i
e1₆(h1₁(w), h2₁(w), x, y, z, w) -> e2₆(x, x, y, z, z, w)
e1₆(x1, x1, x, y, z, a) -> e5₄(x1, x, y, z)
e2₆(f1₂(w, w), x, y, z, f2₂(w, w), w) -> e3₁₂(x, y, x, y, y, z, y, z, x, y, z, w)
e2₆(x, x, y, z, z, a) -> e6₃(x, y, z)
e2₆(i, x, y, z, i, a) -> e6₃(x, y, z)
e3₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> e4₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3₁₂(x, y, x, y, y, z, y, z, x, y, z, a) -> e6₃(x, y, z)
e4₁₂(g1₂(w, w), x1, g2₂(w, w), x1, g1₂(w, w), x1, g2₂(w, w), x1, x, y, z, w) -> e1₆(x1, x1, x, y, z, w)
e4₁₂(i, x1, i, x1, i, x1, i, x1, x, y, z, a) -> e5₄(x1, x, y, z)
e4₁₂(x, x, x, x, x, x, x, x, x, x, x, a) -> e6₃(x, x, x)
e5₄(i, x, y, z) -> e6₃(x, y, z)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

G2₂(x, a) -> H2₁(x)
E4₁₂(g1₂(w, w), x1, g2₂(w, w), x1, g1₂(w, w), x1, g2₂(w, w), x1, x, y, z, w) -> E1₆(x1, x1, x, y, z, w)
E4₁₂(i, x1, i, x1, i, x1, i, x1, x, y, z, a) -> E5₄(x1, x, y, z)
F1₂(x, a) -> G2₂(x, x)
G1₂(x, a) -> H2₁(x)
E1₆(h1₁(w), h2₁(w), x, y, z, w) -> E2₆(x, x, y, z, z, w)
E2₆(f1₂(w, w), x, y, z, f2₂(w, w), w) -> E3₁₂(x, y, x, y, y, z, y, z, x, y, z, w)
E3₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> E4₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
F2₂(a, x) -> G1₂(x, x)
G2₂(a, x) -> H1₁(x)
F1₂(a, x) -> G1₂(x, x)
F2₂(x, a) -> G2₂(x, x)
G1₂(a, x) -> H1₁(x)
E1₆(x1, x1, x, y, z, a) -> E5₄(x1, x, y, z)

The TRS R consists of the following rules:

f1₂(a, x) -> g1₂(x, x)
f1₂(x, a) -> g2₂(x, x)
f2₂(a, x) -> g1₂(x, x)
f2₂(x, a) -> g2₂(x, x)
g1₂(a, x) -> h1₁(x)
g1₂(x, a) -> h2₁(x)
g2₂(a, x) -> h1₁(x)
g2₂(x, a) -> h2₁(x)
h1₁(a) -> i
h2₁(a) -> i
e1₆(h1₁(w), h2₁(w), x, y, z, w) -> e2₆(x, x, y, z, z, w)
e1₆(x1, x1, x, y, z, a) -> e5₄(x1, x, y, z)
e2₆(f1₂(w, w), x, y, z, f2₂(w, w), w) -> e3₁₂(x, y, x, y, y, z, y, z, x, y, z, w)
e2₆(x, x, y, z, z, a) -> e6₃(x, y, z)
e2₆(i, x, y, z, i, a) -> e6₃(x, y, z)
e3₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> e4₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3₁₂(x, y, x, y, y, z, y, z, x, y, z, a) -> e6₃(x, y, z)
e4₁₂(g1₂(w, w), x1, g2₂(w, w), x1, g1₂(w, w), x1, g2₂(w, w), x1, x, y, z, w) -> e1₆(x1, x1, x, y, z, w)
e4₁₂(i, x1, i, x1, i, x1, i, x1, x, y, z, a) -> e5₄(x1, x, y, z)
e4₁₂(x, x, x, x, x, x, x, x, x, x, x, a) -> e6₃(x, x, x)
e5₄(i, x, y, z) -> e6₃(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

G2₂(x, a) -> H2₁(x)
E4₁₂(g1₂(w, w), x1, g2₂(w, w), x1, g1₂(w, w), x1, g2₂(w, w), x1, x, y, z, w) -> E1₆(x1, x1, x, y, z, w)
E4₁₂(i, x1, i, x1, i, x1, i, x1, x, y, z, a) -> E5₄(x1, x, y, z)
F1₂(x, a) -> G2₂(x, x)
G1₂(x, a) -> H2₁(x)
E1₆(h1₁(w), h2₁(w), x, y, z, w) -> E2₆(x, x, y, z, z, w)
E2₆(f1₂(w, w), x, y, z, f2₂(w, w), w) -> E3₁₂(x, y, x, y, y, z, y, z, x, y, z, w)
E3₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> E4₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
F2₂(a, x) -> G1₂(x, x)
G2₂(a, x) -> H1₁(x)
F1₂(a, x) -> G1₂(x, x)
F2₂(x, a) -> G2₂(x, x)
G1₂(a, x) -> H1₁(x)
E1₆(x1, x1, x, y, z, a) -> E5₄(x1, x, y, z)

The TRS R consists of the following rules:

f1₂(a, x) -> g1₂(x, x)
f1₂(x, a) -> g2₂(x, x)
f2₂(a, x) -> g1₂(x, x)
f2₂(x, a) -> g2₂(x, x)
g1₂(a, x) -> h1₁(x)
g1₂(x, a) -> h2₁(x)
g2₂(a, x) -> h1₁(x)
g2₂(x, a) -> h2₁(x)
h1₁(a) -> i
h2₁(a) -> i
e1₆(h1₁(w), h2₁(w), x, y, z, w) -> e2₆(x, x, y, z, z, w)
e1₆(x1, x1, x, y, z, a) -> e5₄(x1, x, y, z)
e2₆(f1₂(w, w), x, y, z, f2₂(w, w), w) -> e3₁₂(x, y, x, y, y, z, y, z, x, y, z, w)
e2₆(x, x, y, z, z, a) -> e6₃(x, y, z)
e2₆(i, x, y, z, i, a) -> e6₃(x, y, z)
e3₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> e4₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3₁₂(x, y, x, y, y, z, y, z, x, y, z, a) -> e6₃(x, y, z)
e4₁₂(g1₂(w, w), x1, g2₂(w, w), x1, g1₂(w, w), x1, g2₂(w, w), x1, x, y, z, w) -> e1₆(x1, x1, x, y, z, w)
e4₁₂(i, x1, i, x1, i, x1, i, x1, x, y, z, a) -> e5₄(x1, x, y, z)
e4₁₂(x, x, x, x, x, x, x, x, x, x, x, a) -> e6₃(x, x, x)
e5₄(i, x, y, z) -> e6₃(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 10 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

E4₁₂(g1₂(w, w), x1, g2₂(w, w), x1, g1₂(w, w), x1, g2₂(w, w), x1, x, y, z, w) -> E1₆(x1, x1, x, y, z, w)
E1₆(h1₁(w), h2₁(w), x, y, z, w) -> E2₆(x, x, y, z, z, w)
E2₆(f1₂(w, w), x, y, z, f2₂(w, w), w) -> E3₁₂(x, y, x, y, y, z, y, z, x, y, z, w)
E3₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> E4₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)

The TRS R consists of the following rules:

f1₂(a, x) -> g1₂(x, x)
f1₂(x, a) -> g2₂(x, x)
f2₂(a, x) -> g1₂(x, x)
f2₂(x, a) -> g2₂(x, x)
g1₂(a, x) -> h1₁(x)
g1₂(x, a) -> h2₁(x)
g2₂(a, x) -> h1₁(x)
g2₂(x, a) -> h2₁(x)
h1₁(a) -> i
h2₁(a) -> i
e1₆(h1₁(w), h2₁(w), x, y, z, w) -> e2₆(x, x, y, z, z, w)
e1₆(x1, x1, x, y, z, a) -> e5₄(x1, x, y, z)
e2₆(f1₂(w, w), x, y, z, f2₂(w, w), w) -> e3₁₂(x, y, x, y, y, z, y, z, x, y, z, w)
e2₆(x, x, y, z, z, a) -> e6₃(x, y, z)
e2₆(i, x, y, z, i, a) -> e6₃(x, y, z)
e3₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) -> e4₁₂(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3₁₂(x, y, x, y, y, z, y, z, x, y, z, a) -> e6₃(x, y, z)
e4₁₂(g1₂(w, w), x1, g2₂(w, w), x1, g1₂(w, w), x1, g2₂(w, w), x1, x, y, z, w) -> e1₆(x1, x1, x, y, z, w)
e4₁₂(i, x1, i, x1, i, x1, i, x1, x, y, z, a) -> e5₄(x1, x, y, z)
e4₁₂(x, x, x, x, x, x, x, x, x, x, x, a) -> e6₃(x, x, x)
e5₄(i, x, y, z) -> e6₃(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.